Inference at * 1 1 1 
Iof proof for Lemma dep ax choice:



1. A : Type
2. B : AType
3. Q : x:AB(x)Type
4. g : x:Ay:B(x)  Q(x,y)
5. x : A
  Q(x,(g(x)).1) 

latex

 by ((With x (D 4)) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 6. y : y:B(x)  Q(x,y)
C1: 7. y = g(x)
C1:   Q(x,(g(x)).1)
C.

Definitions

t  T